# kinds [for builtin theory]                                          -*- sh -*-
#
# This "kinds" file is written in a domain-specific language for
# declaring cvc5 kinds.  Comments are marked with #, as this line is.
#
# The first non-blank, non-comment line in this file must be a theory
# declaration:
#
#   theory ID T header
#
#     Thereafter, ID is bound to your theory.  It becomes part of an
#     enumeration that identifies all theories.  If your theory has
#     several, distinct implementations, they still all share a kinds
#     file, a theory ID, all the defined kinds/operators/types for the
#     theory, typechecker, etc.  They should also share a base class
#     (that's the T above).  The header is the header for this base
#     class.
#
# The very end of this file should end with:
#
#   endtheory
#
# There are several basic commands:
#
#   properties PROPERTIES...
#
#     This command declares properties of the theory.  It can occur
#     more than once, in which case the effect is additive.
#
#     The current set of properties and their meanings are:
#
#       finite            the theory is finite
#       stable-infinite   the theory is stably infinite
#       polite            the theory is polite
#       parametric        the theory is parametric
#
#       check             the theory supports the check() function
#       propagate         the theory supports propagate() (and explain())
#       ppStaticLearn     the theory supports ppStaticLearn()
#       notifyRestart     the theory supports notifyRestart()
#       presolve          the theory supports presolve()
#       postsolve         the theory supports postsolve()
#
#     In the case of the "theory-supports-function" properties, you
#     need to declare these for your theory or the functions will not
#     be called!  This is used to speed up the core where functionality
#     is not needed.
#
#   rewriter T header
#
#     This declares a rewriter class T for your theory, declared in
#     header.  Your rewriter class provides four functions:
#
#       static void init();
#       static void shutdown();
#       static RewriteResponse preRewrite(TNode node);
#       static RewriteResponse postRewrite(TNode node);
#
#     ...BUT please note that init() and shutdown() may be removed in
#     future, so if possible, do not rely on them being called (and
#     implement them as a no-op).
#
#   typechecker header
#
#     Declare that this theory's typechecker class is defined in the
#     given header.  (#include'd by the TypeChecker class in the expr
#     package.)
#
#   variable K ["comment"]
#
#     This declares a kind K that has no operator (it's conceptually a
#     VARIABLE).  This is appropriate for things like VARIABLE and
#     SKOLEM.
#
#   operator K #children ["comment"]
#
#     Declares a "built-in" operator kind K.  Really this is the same
#     as "variable" except that it has an operator (automatically
#     generated by NodeManager).
#
#     You can specify an exact # of children required as the second
#     argument to the operator command.  In debug mode, assertions are
#     automatically included to ensure that no Nodes can ever be
#     created violating this.  (FIXME: the public Expr stuff should
#     enforce them regardless of whether debugging or not.)  For
#     example, a binary operator could be specified as:
#
#         operator LESS_THAN 2 "arithmetic comparison, x < y"
#
#     Alternatively, a range can be specified for #children as
#     "LB:[UB]", LB and UB representing lower and upper bounds on the
#     number of children (inclusive).  If there is no lower bound, put
#     a "1" (operators must have at least one child).  If there is no
#     upper bound, leave the colon after LB, but omit UB.  For example,
#     an N-ary operator might be defined as:
#
#         operator ADD 2: "addition on two or more arguments"
#
#   parameterized K1 K2 #children ["comment"]
#
#     Declares a "built-in" parameterized operator kind K1.  This is a
#     theory-specific APPLY, e.g., APPLY_UF, which applies its first
#     parameter (say, "f"), to its operands (say, "x" and "y", making
#     the full application "f(x,y)").  Nodes with such a kind will
#     have an operator (Node::hasOperator() returns true, and
#     Node::getOperator() returns the Node of functional type
#     representing "f" here), and the "children" are defined to be
#     this operator's parameters, and don't include the operator
#     itself (here, there are only two children "x" and "y").  The
#     operator ("f") should have kind K2 (and this should be enforced
#     by the custom typechecker, at present this isn't done uniformly
#     by the expression package).
#
#     LB and UB are the same as documented for the operator command,
#     except that parameterized operators may have zero children.  The
#     first parameter (the function being applied) does not count as a
#     child.
#
#     For consistency these should start with "APPLY_", but this is
#     not enforced.
#
#   constant K F T Hasher header ["comment"]
#
#     Declares a constant kind K.  F is the type of the forward declaration to
#     generate (e.g., `class`, `struct`). If F is `skip` then then no forward
#     declaration is generated.  T is the C++ type representing the constant
#     internally (the type is expected to be in the cvc5 namespace), and header
#     is the header needed to define it.  Hasher is a hash functor type defined
#     like this:
#
#       struct MyHashFcn {
#         size_t operator()(const T& val) const;
#       };
#
#     For consistency, constants taking a non-void payload should
#     start with "CONST_", but this is not enforced.
#
#   typerule K typechecker-class
#
#     Declares that a (previously-declared) kind K is typechecked by
#     the typechecker-class.  This class should be defined by the
#     header given to the "typechecker" command, above.  The
#     typechecker-class is used this way by the main TypeChecker code:
#
#       typechecker-class::computeType(NodeManager* nm, TNode n, bool check)
#
#     It returns TypeNode.  It should compute the type of n and return it,
#     and if "check" is true, should actually perform type checking instead
#     of simply type computation.
#
#   sort K cardinality [well-founded ground-term header | not-well-founded] ["comment"]
#
#     This creates a kind K that represents a sort (a "type constant").
#     These kinds of types are "atomic" types; if you need to describe
#     a complex type that takes type arguments (like arrays), use
#     "operator"; if you need to describe one that takes "constant"
#     arguments (like bitvectors), use "constant", and if you invent
#     one that takes both, you could try "parameterized".  In those
#     cases, you'll want to provide a cardinality separately for your
#     type.
#
#     The cardinality argument is a nonnegative number (if the sort is
#     finite), or Cardinality::INTEGERS if the sort has the same
#     cardinality as the integers, or Cardinality::REALS if the sort
#     has the same cardinality as the reals.
#
#     If the sort is well-founded (i.e., there exist ground terms),
#     then the argument should be the string "well-founded"; if not,
#     it should be the string "not-well-founded".  If well-founded,
#     two extra arguments immediately follow---a C++ expression that
#     constructs a ground term (as a Node), and the header that must
#     be #included for that expression to compile.
#
#     For consistency, sorts should end with "_TYPE", but this is not
#     enforced.
#
#   cardinality K cardinality-computer [header]
#
#     This command does not define a kind; the kind K needs to be
#     defined by one of the other commands above.  This command just
#     provides a cardinality for types of kind K.  The
#     "cardinality-computer" is a C++ expression that will yield a
#     Cardinality for the type.  In that expression, the sequence of
#     characters "%TYPE%" will be rewritten with a variable containing
#     a TypeNode of kind K.  The optional "header" argument is an
#     include file necessary to compile the cardinality-computer
#     expression.
#
#     If the cardinality need not be computed per-type (i.e., it's the
#     same for all types of kind K, but the "sort" gesture above could
#     not be used---in which case it doesn't already have a registered
#     cardinality), you can simply construct a Cardinality temporary.
#     For example:
#
#       cardinality MY_TYPE Cardinality(Cardinality::INTEGERS)
#
#     If not, you might opt to use a computer; a common place to put it
#     is with your type checker:
#
#       cardinality MY_TYPE \
#           ::cvc5::internal::theory::foo::TheoryFoo::CardinalityComputer(%TYPE%) \
#           "theory/foo/theory_foo_type_rules.h"
#
#   well-founded K wellfoundedness-computer ground-term-computer [header]
#
#     Analogous to the "cardinality" command above, the well-founded
#     command provides a well-foundedness computer for the type.  A
#     ground term computer is required unless the
#     wellfoundedness-computer is the constant "false".  The ground
#     term computer should return a Node, and it should return the
#     same Node each time for a given type (although usually it's only
#     ever called once anyway since the result is cached).
#
#
# Lines may be broken with a backslash between arguments; for example:
#
#     constant CONST_INT \
#         int IntHash \
#         "" \
#         "This is a constant representing an INT.
#         Its payload is the C++ int type.
#         It is used by the theory of arithmetic."
#
# As shown in the example, ["comment"] fields may be broken across
# multiple lines too.
#
# The expr package guarantees that Nodes built with kinds have the
# following constraints imposed on them.  (The #children guarantee
# only holds when assertions are turned on.)
#
#   Node meta-kind      has operator?      # children
#   ==================  =================  =======================
#   variable            no                 zero
#   operator            yes                as documented above
#   parameterized       yes                as documented above
#   constant            no                 zero
#
# NOTE THAT This file is actually an executable Bourne shell script
# (sourced by the processing scripts after defining functions called
# "theory," "variable," "operator," "parameterized," and "constant").
# Please don't do anything else in this file other than using these
# commands.
#

theory THEORY_BUILTIN ::cvc5::internal::theory::builtin::TheoryBuiltin "theory/builtin/theory_builtin.h"
typechecker "theory/builtin/theory_builtin_type_rules.h"

properties stable-infinite

# Rewriter responsible for all the terms of the theory
rewriter ::cvc5::internal::theory::builtin::TheoryBuiltinRewriter "theory/builtin/theory_builtin_rewriter.h"

sort BUILTIN_OPERATOR_TYPE \
    Cardinality::INTEGERS \
    not-well-founded \
    "the type for built-in operators"

variable SORT_TYPE "specifies types of user-declared 'uninterpreted' sorts"
# The cardinality of uninterpreted sorts is defined infinite here, although they are given special treatment in TypeNode::getCardinalityClass
cardinality SORT_TYPE "Cardinality(Cardinality::INTEGERS)"
well-founded SORT_TYPE \
    "::cvc5::internal::theory::builtin::SortProperties::isWellFounded(%TYPE%)" \
    "::cvc5::internal::theory::builtin::SortProperties::mkGroundTerm(%TYPE%)" \
    "theory/builtin/theory_builtin_type_rules.h"
enumerator SORT_TYPE ::cvc5::internal::theory::builtin::UninterpretedSortEnumerator "theory/builtin/type_enumerator.h"

# an instantiated sort has the same properties as an ordinary uninterpreted sort
operator INSTANTIATED_SORT_TYPE 1: "instantiated uninterpreted sort"
cardinality INSTANTIATED_SORT_TYPE "Cardinality(Cardinality::INTEGERS)"
well-founded INSTANTIATED_SORT_TYPE \
    "::cvc5::internal::theory::builtin::SortProperties::isWellFounded(%TYPE%)" \
    "::cvc5::internal::theory::builtin::SortProperties::mkGroundTerm(%TYPE%)" \
    "theory/builtin/theory_builtin_type_rules.h"
enumerator INSTANTIATED_SORT_TYPE ::cvc5::internal::theory::builtin::UninterpretedSortEnumerator "theory/builtin/type_enumerator.h"

constant UNINTERPRETED_SORT_VALUE \
    class \
    UninterpretedSortValue \
    ::cvc5::internal::UninterpretedSortValueHashFunction \
    "util/uninterpreted_sort_value.h" \
    "the kind of expressions representing uninterpreted sort values; payload is an instance of the cvc5::internal::AbstractValue class (used in models)"
typerule UNINTERPRETED_SORT_VALUE ::cvc5::internal::theory::builtin::UninterpretedSortValueTypeRule

# A kind representing "inlined" operators defined with OPERATOR
# Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's
# not stored that way.  If you ask for the operator of (EQUAL a b),
# you'll get a special, singleton (BUILTIN EQUAL) Node.
constant BUILTIN \
    skip \
    Kind \
    ::cvc5::internal::kind::KindHashFunction \
    "expr/kind.h" \
    "the kind of expressions representing built-in operators"

operator EQUAL 2 "equality (two parameters only, sorts must match)"
operator DISTINCT 2: "disequality (N-ary, sorts must match)"
variable VARIABLE "a variable (not permitted in bindings)"
variable BOUND_VARIABLE "a bound variable (permitted in bindings and the associated lambda and quantifier bodies only)"
variable SKOLEM "a Skolem variable (internal only)"
operator SEXPR 0: "a symbolic expression (any arity)"

operator WITNESS 2:3 "a witness expression; first parameter is a BOUND_VAR_LIST, second is the witness body"

constant TYPE_CONSTANT \
    skip \
    TypeConstant \
    ::cvc5::internal::TypeConstantHashFunction \
    "expr/kind.h" \
    "a representation for basic types"
sort SEXPR_TYPE \
    Cardinality::INTEGERS \
    not-well-founded \
    "the type of a symbolic expression"

typerule EQUAL ::cvc5::internal::theory::builtin::EqualityTypeRule
typerule DISTINCT ::cvc5::internal::theory::builtin::DistinctTypeRule
typerule SEXPR ::cvc5::internal::theory::builtin::SExprTypeRule
typerule WITNESS ::cvc5::internal::theory::builtin::WitnessTypeRule

variable RAW_SYMBOL "a variable that is not quoted in the smt2 printer (internal only)"


constant ABSTRACT_TYPE \
  class \
  AbstractType \
  ::cvc5::internal::AbstractTypeHashFunction \
  "theory/builtin/abstract_type.h" \
  "abstract type"
cardinality ABSTRACT_TYPE "Cardinality(Cardinality::INTEGERS)"

constant APPLY_INDEXED_SYMBOLIC_OP \
  class \
  GenericOp \
  ::cvc5::internal::GenericOpHashFunction \
  "theory/builtin/generic_op.h" \
  "operator for the bit-vector extract; payload is an instance of the cvc5::internal::GenericOp class"
parameterized APPLY_INDEXED_SYMBOLIC APPLY_INDEXED_SYMBOLIC_OP 1: "generic indexed operator, whose arguments are the list of terms corresponding to (symbolic) indices to the operator followed by its normal arguments"

typerule APPLY_INDEXED_SYMBOLIC_OP "SimpleTypeRule<RBuiltinOperator>"
typerule APPLY_INDEXED_SYMBOLIC ::cvc5::internal::theory::builtin::ApplyIndexedSymbolicTypeRule


# constants
constant SORT_TO_TERM \
  class \
  SortToTerm \
  ::cvc5::internal::SortToTermHashFunction \
  "expr/sort_to_term.h" \
  "term representing a sort; payload is an instance of the cvc5::internal::SortToTerm class"
typerule SORT_TO_TERM "SimpleTypeRule<RBuiltinOperator>"

endtheory
